$\forall$$M$:MsgA, $l$:IdLnk, ${\it tg}$:Id. rcv($l$,${\it tg}$) declared in $M$ $\in$ Prop